Nuprl Lemma : settype-inherence
0,22
postcript
pdf
T
:Type,
P
:(
T
Prop),
x
:{
t
:
T
|
P
(
t
) },
a
:Atom1.
AtomFree(Type;
T
)
AtomFree(
T
Prop;
P
)
x
:
T
>>
a
x
:{
t
:
T
|
P
(
t
) }>>
a
latex
Definitions
x
:
A
.
B
(
x
)
,
Prop
,
x
(
s
)
,
P
Q
,
t
T
Lemmas
subtype-inherence
,
inheres
wf
,
atom-free
wf
origin
T:Type, P:(T
Prop), x:{t:T| P(t) }, a:Atom1.
AtomFree(TProp;P) x:T>>a x:{t:T| P(t) }>>a T:Type, P:(TProp), x:{t:T| P(t) }, a:Atom1.
AtomFree(TProp;P) x:T>>a x:{t:T| P(t) }>>a x:A. B(x) Q
T